|
|
1.
基于Kripke结构的程序正确性证明
林杰 余建坤
计算机应用
2011, 31 (05):
1425-1427.
DOI: 10.3724/SP.J.1087.2011.01425
为了方便证明程序的正确性,引入了Kripke结构,提出基于Kripke结构的程序正确性证明。重新定义了适合证明的Kripke结构,并描述了将程序流程图转换为Kripke结构状态图的方法。给出了证明程序正确性的相关定理和基于Kripke结构的程序正确性证明方法。证明方法为:首先,把程序流程图转换为状态图;然后,根据状态之间的转移关系列出每个状态下的状态谓词;最后,证明每个状态谓词为真。根据状态谓词进行证明,能够反映出程序执行的状态。用该方法对一个实例进行了完整的证明。
相关文章 |
多维度评价
|
|
